The present invention relates generally to hardware verification for electronic circuit designs. More particularly, the present invention relates to model checking and bounded model checking techniques for such verification.
Recent advances in the design of application specific integrated circuits (ASIC) and system-on-chip (SoC) circuits are producing circuit designs of rapidly increasing complexity. These designs are driving the search for techniques that are capable of verifying such complex designs.
Two commonly-used verification techniques are simulation and formal verification. Simulation involves driving test vectors into a behavioral representation of the design and monitoring the response. However, because the number of test vectors required for complete coverage rises exponentially with the number of input bits and state bits (flip-flops) in the design, simulation can explore only a very small portion of the possible traces of a design. For example, a design that has only 40 input bits and 40 state bits would require billions of years of simulation time for complete coverage.
In contrast, model checking employs exhaustive mathematical techniques to prove whether a property holds true for a given design. A model checker uses a model of the design to consider all possible input combinations, and covers all possible reachable states to verify the property. This is possible due to efficient techniques such as Boolean satisfiability engines used in model checkers that allow analysis of sets of states simultaneously, and only consider the logic in the cone of influence of the property the tool is verifying. A bounded model checker, like any model checker, employs exhaustive mathematical techniques to prove whether a property holds true for a given design, but only until some certain cycle k.